COMMENT ⊗   VALID 00004 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.device xgp
C00005 00003	%BMATHEMATICAL THEORY OF COMPUTATION%*
C00014 00004	∧3.  Current Research∨
C00025 ENDMK
C⊗;
.device xgp
.!XGPCOMMANDS ← "/TMAR=200/PMAR=1900/BMAR=100"
.turn on "α";
.font 1 "basl30"; font 2 "basi30";
.AT "ffi" ⊂ IF 0<THISFONT≤2 THEN "α≠"  ELSE "fαfαi" ⊃;
.AT "ffl" ⊂ IF 0<THISFONT≤2 THEN "α∞" ELSE "fαfαl" ⊃;
.AT "ff"  ⊂ IF 0<THISFONT≤2 THEN "α≥"  ELSE "fαf" ⊃;
.AT "fi"  ⊂ IF 0<THISFONT≤2 THEN "α≡" ELSE "fαi" ⊃;
.AT "fl"  ⊂ IF 0<THISFONT≤2 THEN "α∨"  ELSE "fαl" ⊃;
.AT "--"  ⊂ IF 0<THISFONT≤2 THEN "α¬" ELSE "-α-" ⊃;
.turn on "%,π,α,↓_,#,→"
.turn on "∩" for "↑"
.turn on "∪" for "↓"
.turn on "$" for "{"
.TURN ON "@" FOR "α"
.font 3 "NONMB";
.FONT 4 "SUB"
.FONT 5 "SUP"
.FONT 6 "FORN25"
.FONT 7 "FIX25"
.FONT 8 "MISC25"
.FONT 9 "PLUNK"
.FONT A "GRFX25"
.FONT B "CLAR30"
.FONT C "GRKL30"
.FONT D "ngr25"
.FONT E "MATHX[PUB,PAT]"
.FONT F "NGI25"
.FONT G "MS25"
.FONT H "APL25"
.SPACING 10*5 MILLS;
.PAGE FRAME 45 HIGH 78 WIDE
.TITLE AREA HEADING LINES 1 TO 2
.AREA TEXT LINES 3 TO 43
.SELECT 1
.TITLE AREA FOOTING LINES 45
.AT "[" TXT "]"; ⊂("%2TXT%1")⊃;
.at "≤" ⊂"%7α≤%*"⊃
.at "≥" ⊂"%7α≥%*"⊃
.at "↓" txt "↑" ⊂"%4txt%*"⊃
.at "↑" txt "↓" ⊂"%5txt%*"⊃
.at "!cd" ⊂"%7π.%*"⊃
.at "!'" ⊂"%8α'%*"⊃
.at "!ε" ⊂"%7αε%*"⊃
.at "!{" ⊂"%3α{%*"⊃
.at "!}" ⊂"%3α}%*"⊃
.at "$⊗" ⊂skip;"%Eα⊗%*"⊃
.at "-" ⊂"%6α-%*"⊃
.at "¬" ⊂"%6α¬%*"⊃
.at "<=>" ⊂"%7α<α=α>%*"⊃
.at "=>" ⊂"%7α=α>%*"⊃
.at "<=" ⊂"%7α<α=%*"⊃
.at "≠" ⊂"%7α≠%*"⊃
.at "|" ⊂"%6α|%*"⊃
.AT "∞" ⊂"%9α[%*"⊃
.at "∂" ⊂"%9α]%*"⊃
.AT "@" ⊂"%Aαα%*"⊃
.at "∧" TXT "∨"; ⊂"%3TXT%*"⊃;
.macro bi; ⊂
.indent 8,12,8;
.turn on "\"; tabs 13;
. ⊃
.macro bf; ⊂
.crbreak; nojust;
.preface 0; turn on "\";
.tabs 8,17,21;
. ⊃
.macro bl; ⊂
.crbreak; nojust;
.preface 0; turn on "\";
.tabs 4,10,18,21;
. ⊃
.PLACE TEXT
%BMATHEMATICAL THEORY OF COMPUTATION%*
.break
%BA Unified Framework for Program Verification%*
.BREAK
∧Personnel:  John McCarthy, Zohar Manna∨
.skip
∧Students:  Chris Goad, Tod Wagner, Martin Brooks, and Nachum Dershowitz∨
.skip
∧1.  Motivation∨
.skip
In the past decade there has been intense research into the problem of proving
the correctness of computer programs. As a result, a variety of different program
verification techniques have appeared. These methods have different realms of
application: some show partial correctness and others show termination, total
correctness or equivalence; some apply to recursive and others to iterative
programs; some apply to the program itself, but others require that the program
be documented or altered.

Here are some of the principle program verification methods and their applications:
$⊗ [Invariant-assertion method]:  partial correctness of iterative
  programs (Floydα[1967α], Hoareα[1969α])
$⊗ [Well-founded ordering method]:  termination of iterative programs
  (Floydα[1967α])
$⊗ [Structural-induction method]:  total correctness and equivalence of
  recursive programs (Burstallα[1969α])
$⊗ [Subgoal-assertion method]:  partial correctness of iterative and
  recursive programs (Mannaα[1971α], Morris and Wegbreitα[1977α])
$⊗ [Counters method]:  termination of iterative programs (Elspas et
  al.α[1974α], Katz and Mannaα[1976α])
$⊗ [Intermittent-assertion method]:  total correctness of iterative
  programs (Burstallα[1974α], Manna and Waldingerα[1976α]).
.skip 2
Most current verification systems employ only the invariant-assertion method for proving
partial correctness and the counters method for proving termination, even though
for some situations another of the techniques may be decidedly superior.
For instance, these two techniques cannot be applied to verify certain classes
of programs, such as recursive programs, or to prove certain properties, such as
the equivalence of two programs. Furthermore, for some verification problems
another of the techniques may yield significantly simpler proofs than those required by
the two most commonly used methods. 

However, one of the most striking differences
between verification methods is in the nature of the documentation they require
the user to supply.  
Most verification methods require some form of documentation, in which the user expresses
his intuition about how he expects the program to work. However,
different techniques require very different sorts of documentation. Furthermore,
the documentation that is most natural and easy to provide varies in form from
program to program.
.skip 
.skip
∧2.  The Goals∨
.skip
We therefore propose to conduct an investigation with the following goals:
.skip
∧(A) Comparing methods:∨
$⊗  We hope to discover which methods are equivalent in power and which methods
are strictly stronger than others, and
to determine situations in which a given method may yield simpler
proofs than another.
$⊗  We want to compare the documentation requirments of the different methods in
a rigorous way.
Ideally, we wish the user of a verification
system to    be able to document his intuitions in whatever way he finds most
convenient, and have  the system    select the technique that best matches the
program and documentation supplied and the property to be proved.
.skip
.skip
∧(B) Strengthening methods:∨
$⊗  We need to make the existing methods less dependent on the documentation
supplied by the user. Thus, we will devise new ways of generating documentation
automatically, and of altering and extending the documentation supplied by the user.
$⊗  We would like to extend the realm of application of some of the methods, e.g. 
find how to apply the intermittent-assertion method to show the equivalence of
two iterative programs or the correctness of nondeterministic or parallel programs.
$⊗  We hope to develop more general techniques that will be able to draw on the
advantages of all the existing techniques, and compensate for weaknesses in the
existing methodology.
.skip
.skip
∧(C) Finding new applications:∨
We intend to apply
methods devised for program verification to other problems such as:
$⊗  [Development:] constructing a program to meet given specifications
$⊗  [Transformation]: altering a given program to compute the same output in a
different way, generally in order to optimize the program.
$⊗  [Modification:] altering a given program to debug it, to adapt it to meet
revised specifications, or to extend its capabilities.
.skip

∧3.  Current Research∨

$⊗ ∧Unified Framework∨ 

JOHN McCARTHY
.skip
$⊗ ∧Program Annotation∨

[ZOHAR MANNA] investigates techniques by which an Algol-like program, given
together with its input-output specifications, may be documented automatically.
This documentation expresses invariant relationships that hold between program 
variables at intermediate points in the program, and explains the acutal workings
of the program regardless of whether the program is correct.  Thus this documentation
can be used for proving the correctness of the program, or may serve as an aid
in the debugging of an incorrect program.

He recently succeeded in unifying existing approaches to this problem, and improving
most of the known methods.  The techniques are expressed as rules which derive
invariants from the assignment statements in from the control structure of the
program, and as heuristics which propose relationships whose invariance must be
verified.  The implementation of this system is in progress.

Earlier results along this line have appeared in a paper by S. Katz and Z. Manna
(Communication of the ACM, Vol. 19, No. 4, April 1976).
.skip
$⊗ ∧Program Modification∨

[NACHUM DERSHOWITZ] (graduate student) attempts to formulate techniques of program
modification, whereby a program that achieves one result can be transformed into
a new program that uses the same principles to achieve a different goal.  For
example, a program that uses the binary search paradigm to calulate the square-root
of a number may be modified to divide two numbers in a similar manner, or vice versa.

The essence of the approach lies in the ability to formulate an [analogy] between
two sets of specifications, those of a program that has already been constructed
and those of the program that we desire to construct.  The analogy is then used
as the basis for transforming the existing program to meet the new specifications.

Program debugging is considered as an important special case of program modification:
the properties of an incorrect program are compared with the specifications, and 
a modification (correction) sought that transforms the incorrect program into a
correct one.

This approach has been embedded in an experimental implmentation and was presented
by N. Dershowitz and Z. Manna at the Conference on Principles of Programming 
Languages (Los Angeles, Ca., January 1977).
.skip
$⊗ ∧The Intermittent∨-∧Assertion Method∨

[ZOHAR MANNA] explored a new technique for proving the correctness and termination
of programs simultaneously.  This approach, which he calls the [intermittent]-[assertion]
method, involves documenting the program with assertions that must be true at some
time when control passes through the corresponding point, but that need not be true
every time.  The method, introduced by Burstall α[1974α], promises to provide a
valuable complement to the more conventional methods.

On all the examples he tried,
the intermittent-assetion proofs turned to be simpler than their
conventional counterparts.  On the other hand, he showed that a proof of correctness
or termination by any of the conventional techniques can be rephrased directly as
a proof using intermittent-assertions.
The intermittent-assertin method can also be 
applied to prove the validity of program transformations and the correctness of
continuously operating programs.

This work is described in a recent paper by Z. Manna and R. Waldinger (to be
published in the Communication of the ACM).  Manna and Waldinger believe that the
intermittent-assertion method will have practical impact because it often allows
one to incorporate his intuitive understanding about the way a program works
directly into a proof of its correctness.
.skip
$⊗∧Hardware Verification∨

The research of [TODD WAGNER] (graduate student)
involves developing methods for detecting logical errors in
hardware designs using symbolic manipulation techniques instead of
simulation.  A very simple register transfer language has been proposed
which can be used to specify the desired behaviour of a digital system.
The same language can also be used to describe the individual components
used in the design.  A series of logical transformations can then be used
to prove that the set of interconnected components correctly satisfy the
specifications for the overall system.

The process of hardware verification uses the basic boolean
identities derived from switching theory along with some techniques for
determining the possible effects of clock transitions as they move thru a
circuit.  Methods for detecting timing anomalies such as races, hazards,
and oscillations have also been studied.

A major goal of this research is to be able deal with fairly complex
large scale integrated
components without having to reduce their descriptions to the gate
level.  For example, if a designer requires several complex operations and
uses a microprocessor in his circuit, it should only be necessary to
demonstrate that the required operations are included in the
microprocessor instruction set and that the timing and control logic are
correct.  Current methods would require a gate level model of the
microprocessor and fairly exhaustive simulation.  As components become
more complex it will become increasingly advantageous to prove circuit
correctness algebraically and at a fairly high level.

Preliminary results were presented at the Symposium on Design Automation and
Microprocessors (Palo Alto, Ca., February 1977).
.skip
$⊗ ∧Automatic Debbuging∨

MARTIN BROOKS is currently developing methods for specifying and analyzing
LISP programs, considering both the theoretical and practical aspects. One
goal of this research is the design and implementation of an automatic LISP
debugging system.

The automatic debugger is initially supplied with an undebugged program. The
system then analyzes the program by symbolic evaluation and automatically 
generates a sufficient [finite] set of test inputs for which the user supplies 
the intended outputs. The system extracts the structure of the undebugged program
and then use the input-output pairs to fill out the missing details (re-synthesis), 
yielding a new debugged program.

The main advantage of this approach is that it does not require the user to give
a formal specification, usually a difficult and error-prone task.

The emphasis of Brooks' research will be to develop a general theory for finding
a finite set of input-output pairs which represent a complete specification
of a program,
depending on the structure of the program. 
.break
$⊗  CHRIS GOAD